es:ES, P, Q:(E), f:({e:E| P(e)} {e:E| Q(e)} ), T, T':Type, R:(TT').
(e:E. P(e)  (valtype(e) r T))
 (e:E. Q(e)  (valtype(e) r T'))
 ((e.P(e) e.f(e) e.Q(e)) with R  ) 

latex

Definitions	P  Q, A c B, e c e', P & Q, (e.P(e) a.f(a) e'.Q(e')) with R, t  T, P  Q, x(s), , x:A. B(x)
Lemmas	event system wf, es-valtype wf, es-val wf, es-causl wf, es-E wf, biject wf